(0) Obligation:
Clauses:
half(0, 0).
half(s(0), 0).
half(s(s(X)), s(Y)) :- half(X, Y).
log(0, s(0)).
log(s(X), s(Y)) :- ','(half(s(X), Z), log(Z, Y)).
Query: log(g,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
halfB(s(s(X1)), s(X2)) :- halfB(X1, X2).
logA(s(s(X1)), s(X2)) :- halfB(X1, X3).
logA(s(s(X1)), s(X2)) :- ','(halfcB(X1, X3), logA(s(X3), X2)).
Clauses:
logcA(0, s(0)).
logcA(s(0), s(s(0))).
logcA(s(s(X1)), s(X2)) :- ','(halfcB(X1, X3), logcA(s(X3), X2)).
halfcB(0, 0).
halfcB(s(0), 0).
halfcB(s(s(X1)), s(X2)) :- halfcB(X1, X2).
Afs:
logA(x1, x2) = logA(x1)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
logA_in: (b,f)
halfB_in: (b,f)
halfcB_in: (b,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
LOGA_IN_GA(s(s(X1)), s(X2)) → U2_GA(X1, X2, halfB_in_ga(X1, X3))
LOGA_IN_GA(s(s(X1)), s(X2)) → HALFB_IN_GA(X1, X3)
HALFB_IN_GA(s(s(X1)), s(X2)) → U1_GA(X1, X2, halfB_in_ga(X1, X2))
HALFB_IN_GA(s(s(X1)), s(X2)) → HALFB_IN_GA(X1, X2)
LOGA_IN_GA(s(s(X1)), s(X2)) → U3_GA(X1, X2, halfcB_in_ga(X1, X3))
U3_GA(X1, X2, halfcB_out_ga(X1, X3)) → U4_GA(X1, X2, logA_in_ga(s(X3), X2))
U3_GA(X1, X2, halfcB_out_ga(X1, X3)) → LOGA_IN_GA(s(X3), X2)
The TRS R consists of the following rules:
halfcB_in_ga(0, 0) → halfcB_out_ga(0, 0)
halfcB_in_ga(s(0), 0) → halfcB_out_ga(s(0), 0)
halfcB_in_ga(s(s(X1)), s(X2)) → U8_ga(X1, X2, halfcB_in_ga(X1, X2))
U8_ga(X1, X2, halfcB_out_ga(X1, X2)) → halfcB_out_ga(s(s(X1)), s(X2))
The argument filtering Pi contains the following mapping:
logA_in_ga(
x1,
x2) =
logA_in_ga(
x1)
s(
x1) =
s(
x1)
halfB_in_ga(
x1,
x2) =
halfB_in_ga(
x1)
halfcB_in_ga(
x1,
x2) =
halfcB_in_ga(
x1)
0 =
0
halfcB_out_ga(
x1,
x2) =
halfcB_out_ga(
x1,
x2)
U8_ga(
x1,
x2,
x3) =
U8_ga(
x1,
x3)
LOGA_IN_GA(
x1,
x2) =
LOGA_IN_GA(
x1)
U2_GA(
x1,
x2,
x3) =
U2_GA(
x1,
x3)
HALFB_IN_GA(
x1,
x2) =
HALFB_IN_GA(
x1)
U1_GA(
x1,
x2,
x3) =
U1_GA(
x1,
x3)
U3_GA(
x1,
x2,
x3) =
U3_GA(
x1,
x3)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x1,
x3)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LOGA_IN_GA(s(s(X1)), s(X2)) → U2_GA(X1, X2, halfB_in_ga(X1, X3))
LOGA_IN_GA(s(s(X1)), s(X2)) → HALFB_IN_GA(X1, X3)
HALFB_IN_GA(s(s(X1)), s(X2)) → U1_GA(X1, X2, halfB_in_ga(X1, X2))
HALFB_IN_GA(s(s(X1)), s(X2)) → HALFB_IN_GA(X1, X2)
LOGA_IN_GA(s(s(X1)), s(X2)) → U3_GA(X1, X2, halfcB_in_ga(X1, X3))
U3_GA(X1, X2, halfcB_out_ga(X1, X3)) → U4_GA(X1, X2, logA_in_ga(s(X3), X2))
U3_GA(X1, X2, halfcB_out_ga(X1, X3)) → LOGA_IN_GA(s(X3), X2)
The TRS R consists of the following rules:
halfcB_in_ga(0, 0) → halfcB_out_ga(0, 0)
halfcB_in_ga(s(0), 0) → halfcB_out_ga(s(0), 0)
halfcB_in_ga(s(s(X1)), s(X2)) → U8_ga(X1, X2, halfcB_in_ga(X1, X2))
U8_ga(X1, X2, halfcB_out_ga(X1, X2)) → halfcB_out_ga(s(s(X1)), s(X2))
The argument filtering Pi contains the following mapping:
logA_in_ga(
x1,
x2) =
logA_in_ga(
x1)
s(
x1) =
s(
x1)
halfB_in_ga(
x1,
x2) =
halfB_in_ga(
x1)
halfcB_in_ga(
x1,
x2) =
halfcB_in_ga(
x1)
0 =
0
halfcB_out_ga(
x1,
x2) =
halfcB_out_ga(
x1,
x2)
U8_ga(
x1,
x2,
x3) =
U8_ga(
x1,
x3)
LOGA_IN_GA(
x1,
x2) =
LOGA_IN_GA(
x1)
U2_GA(
x1,
x2,
x3) =
U2_GA(
x1,
x3)
HALFB_IN_GA(
x1,
x2) =
HALFB_IN_GA(
x1)
U1_GA(
x1,
x2,
x3) =
U1_GA(
x1,
x3)
U3_GA(
x1,
x2,
x3) =
U3_GA(
x1,
x3)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x1,
x3)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 4 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
HALFB_IN_GA(s(s(X1)), s(X2)) → HALFB_IN_GA(X1, X2)
The TRS R consists of the following rules:
halfcB_in_ga(0, 0) → halfcB_out_ga(0, 0)
halfcB_in_ga(s(0), 0) → halfcB_out_ga(s(0), 0)
halfcB_in_ga(s(s(X1)), s(X2)) → U8_ga(X1, X2, halfcB_in_ga(X1, X2))
U8_ga(X1, X2, halfcB_out_ga(X1, X2)) → halfcB_out_ga(s(s(X1)), s(X2))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
halfcB_in_ga(
x1,
x2) =
halfcB_in_ga(
x1)
0 =
0
halfcB_out_ga(
x1,
x2) =
halfcB_out_ga(
x1,
x2)
U8_ga(
x1,
x2,
x3) =
U8_ga(
x1,
x3)
HALFB_IN_GA(
x1,
x2) =
HALFB_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
HALFB_IN_GA(s(s(X1)), s(X2)) → HALFB_IN_GA(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
HALFB_IN_GA(
x1,
x2) =
HALFB_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
HALFB_IN_GA(s(s(X1))) → HALFB_IN_GA(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- HALFB_IN_GA(s(s(X1))) → HALFB_IN_GA(X1)
The graph contains the following edges 1 > 1
(13) YES
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
LOGA_IN_GA(s(s(X1)), s(X2)) → U3_GA(X1, X2, halfcB_in_ga(X1, X3))
U3_GA(X1, X2, halfcB_out_ga(X1, X3)) → LOGA_IN_GA(s(X3), X2)
The TRS R consists of the following rules:
halfcB_in_ga(0, 0) → halfcB_out_ga(0, 0)
halfcB_in_ga(s(0), 0) → halfcB_out_ga(s(0), 0)
halfcB_in_ga(s(s(X1)), s(X2)) → U8_ga(X1, X2, halfcB_in_ga(X1, X2))
U8_ga(X1, X2, halfcB_out_ga(X1, X2)) → halfcB_out_ga(s(s(X1)), s(X2))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
halfcB_in_ga(
x1,
x2) =
halfcB_in_ga(
x1)
0 =
0
halfcB_out_ga(
x1,
x2) =
halfcB_out_ga(
x1,
x2)
U8_ga(
x1,
x2,
x3) =
U8_ga(
x1,
x3)
LOGA_IN_GA(
x1,
x2) =
LOGA_IN_GA(
x1)
U3_GA(
x1,
x2,
x3) =
U3_GA(
x1,
x3)
We have to consider all (P,R,Pi)-chains
(15) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LOGA_IN_GA(s(s(X1))) → U3_GA(X1, halfcB_in_ga(X1))
U3_GA(X1, halfcB_out_ga(X1, X3)) → LOGA_IN_GA(s(X3))
The TRS R consists of the following rules:
halfcB_in_ga(0) → halfcB_out_ga(0, 0)
halfcB_in_ga(s(0)) → halfcB_out_ga(s(0), 0)
halfcB_in_ga(s(s(X1))) → U8_ga(X1, halfcB_in_ga(X1))
U8_ga(X1, halfcB_out_ga(X1, X2)) → halfcB_out_ga(s(s(X1)), s(X2))
The set Q consists of the following terms:
halfcB_in_ga(x0)
U8_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(17) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
LOGA_IN_GA(s(s(X1))) → U3_GA(X1, halfcB_in_ga(X1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(LOGA_IN_GA(x1)) = x1
POL(U3_GA(x1, x2)) = 1 + x2
POL(U8_ga(x1, x2)) = 1 + x2
POL(halfcB_in_ga(x1)) = x1
POL(halfcB_out_ga(x1, x2)) = x2
POL(s(x1)) = 1 + x1
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
halfcB_in_ga(0) → halfcB_out_ga(0, 0)
halfcB_in_ga(s(0)) → halfcB_out_ga(s(0), 0)
halfcB_in_ga(s(s(X1))) → U8_ga(X1, halfcB_in_ga(X1))
U8_ga(X1, halfcB_out_ga(X1, X2)) → halfcB_out_ga(s(s(X1)), s(X2))
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GA(X1, halfcB_out_ga(X1, X3)) → LOGA_IN_GA(s(X3))
The TRS R consists of the following rules:
halfcB_in_ga(0) → halfcB_out_ga(0, 0)
halfcB_in_ga(s(0)) → halfcB_out_ga(s(0), 0)
halfcB_in_ga(s(s(X1))) → U8_ga(X1, halfcB_in_ga(X1))
U8_ga(X1, halfcB_out_ga(X1, X2)) → halfcB_out_ga(s(s(X1)), s(X2))
The set Q consists of the following terms:
halfcB_in_ga(x0)
U8_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(19) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(20) TRUE